<!DOCTYPE html PUBLIC "-//IETF//DTD HTML 2.0//EN">
<HTML>
<HEAD>
<TITLE>Enscript Output</TITLE>
</HEAD>
<BODY BGCOLOR="#FFFFFF" TEXT="#000000" LINK="#1F00FF" ALINK="#FF0000" VLINK="#9900DD">
<A NAME="top">
<A NAME="file1">
<H1>Regexp.c</H1>

<PRE>
<I><FONT COLOR="#B22222">/* 
 * Simple regular expression matching.
 *
 * From:
 *   The Practice of Programming
 *   Brian W. Kernighan, Rob Pike
 *
 */</FONT></I> 

#<B><FONT COLOR="#5F9EA0">include</FONT></B> <B><FONT COLOR="#BC8F8F">&lt;klee/klee.h&gt;</FONT></B>

<B><FONT COLOR="#228B22">static</FONT></B> <B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">matchhere</FONT></B>(<B><FONT COLOR="#228B22">char</FONT></B>*,<B><FONT COLOR="#228B22">char</FONT></B>*);

<B><FONT COLOR="#228B22">static</FONT></B> <B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">matchstar</FONT></B>(<B><FONT COLOR="#228B22">int</FONT></B> c, <B><FONT COLOR="#228B22">char</FONT></B> *re, <B><FONT COLOR="#228B22">char</FONT></B> *text) {
  <B><FONT COLOR="#A020F0">do</FONT></B> {
    <B><FONT COLOR="#A020F0">if</FONT></B> (matchhere(re, text))
      <B><FONT COLOR="#A020F0">return</FONT></B> 1;
  } <B><FONT COLOR="#A020F0">while</FONT></B> (*text != <B><FONT COLOR="#BC8F8F">'\0'</FONT></B> &amp;&amp; (*text++ == c || c== <B><FONT COLOR="#BC8F8F">'.'</FONT></B>));
  <B><FONT COLOR="#A020F0">return</FONT></B> 0;
}

<B><FONT COLOR="#228B22">static</FONT></B> <B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">matchhere</FONT></B>(<B><FONT COLOR="#228B22">char</FONT></B> *re, <B><FONT COLOR="#228B22">char</FONT></B> *text) {
  <B><FONT COLOR="#A020F0">if</FONT></B> (re[0] == <B><FONT COLOR="#BC8F8F">'\0'</FONT></B>)
     <B><FONT COLOR="#A020F0">return</FONT></B> 0;
  <B><FONT COLOR="#A020F0">if</FONT></B> (re[1] == <B><FONT COLOR="#BC8F8F">'*'</FONT></B>)
    <B><FONT COLOR="#A020F0">return</FONT></B> matchstar(re[0], re+2, text);
  <B><FONT COLOR="#A020F0">if</FONT></B> (re[0] == <B><FONT COLOR="#BC8F8F">'$'</FONT></B> &amp;&amp; re[1]==<B><FONT COLOR="#BC8F8F">'\0'</FONT></B>)
    <B><FONT COLOR="#A020F0">return</FONT></B> *text == <B><FONT COLOR="#BC8F8F">'\0'</FONT></B>;
  <B><FONT COLOR="#A020F0">if</FONT></B> (*text!=<B><FONT COLOR="#BC8F8F">'\0'</FONT></B> &amp;&amp; (re[0]==<B><FONT COLOR="#BC8F8F">'.'</FONT></B> || re[0]==*text))
    <B><FONT COLOR="#A020F0">return</FONT></B> matchhere(re+1, text+1);
  <B><FONT COLOR="#A020F0">return</FONT></B> 0;
}

<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">match</FONT></B>(<B><FONT COLOR="#228B22">char</FONT></B> *re, <B><FONT COLOR="#228B22">char</FONT></B> *text) {
  <B><FONT COLOR="#A020F0">if</FONT></B> (re[0] == <B><FONT COLOR="#BC8F8F">'^'</FONT></B>)
    <B><FONT COLOR="#A020F0">return</FONT></B> matchhere(re+1, text);
  <B><FONT COLOR="#A020F0">do</FONT></B> {
    <B><FONT COLOR="#A020F0">if</FONT></B> (matchhere(re, text))
      <B><FONT COLOR="#A020F0">return</FONT></B> 1;
  } <B><FONT COLOR="#A020F0">while</FONT></B> (*text++ != <B><FONT COLOR="#BC8F8F">'\0'</FONT></B>);
  <B><FONT COLOR="#A020F0">return</FONT></B> 0;
}

<I><FONT COLOR="#B22222">/*
 * Harness for testing with KLEE.
 */</FONT></I>

<I><FONT COLOR="#B22222">// The size of the buffer to test with.
</FONT></I>#<B><FONT COLOR="#5F9EA0">define</FONT></B> <FONT COLOR="#B8860B">SIZE</FONT> 7

<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">main</FONT></B>() {
  <I><FONT COLOR="#B22222">// The input regular expression.
</FONT></I>  <B><FONT COLOR="#228B22">char</FONT></B> re[SIZE];
  
  <I><FONT COLOR="#B22222">// Make the input symbolic. 
</FONT></I>  klee_make_symbolic_name(re, <B><FONT COLOR="#A020F0">sizeof</FONT></B> re, <B><FONT COLOR="#BC8F8F">&quot;re&quot;</FONT></B>);

  <I><FONT COLOR="#B22222">// Try to match against a constant string &quot;hello&quot;.
</FONT></I>  match(re, <B><FONT COLOR="#BC8F8F">&quot;hello&quot;</FONT></B>);

  <B><FONT COLOR="#A020F0">return</FONT></B> 0;
}
</PRE>
<HR>
<ADDRESS>Generated by <A HREF="http://www.iki.fi/~mtr/genscript/">GNU enscript 1.6.4</A>.</ADDRESS>
</BODY>
</HTML>
